config-antecedent(es;Master;Config;c)
== (e:E(Config). (c(e) < e))
== & (e1, e2:E(Config). (c(e1) < c(e2))  (loc(e1) = loc(e2))  (e1 <loc e2))
== & (e:E(Config).
== & (let m = Master(c(e)) in
== & (let mchain_config_ind(Config(e);(cmconfig?(m))
== & (let & (||cmconfig-list(m)||  1 )
== & (let & loc(e) = hd(cmconfig-list(m));(cmconfig?(m))
== & (let & ((null(cmconfig-list(m))))
== & (let & loc(e) = last(cmconfig-list(m));i.(cmconfig?(m))
== & (let & (index:{0..||cmconfig-list(m)||}
== & (let & (((0 < index)
== & (let & (& loc(e) = cmconfig-list(m)[index]
== & (let & (& i = cmconfig-list(m)[(index - 1)]));i,n.(cmseq?(m))
== & (let & i = cmseq-to(m)
== & (let & loc(e) = cmseq-from(m)
== & (let & n = cmseq-num(m))) 

latex

---

clarification:

config-antecedent(es;Master;Config;c)
== (e:es-E-interface(es;Config). es-causl(es; (c(e)); e))
== & (e1:es-E-interface(es;Config), e2:es-E-interface(es;Config).
== & (es-causl(es; (c(e1)); (c(e2)))
== & ( (es-loc(es; e1) = es-loc(es; e2)  Id)
== & ( es-locl(es; e1; e2))
== & (e:es-E-interface(es;Config).
== & (let m = Master(c(e)) in
== & (let mchain_config_ind(Config(e);(cmconfig?(m))
== & (let & (||cmconfig-list(m)||  1 )
== & (let & es-loc(es; e) = hd(cmconfig-list(m))  Id;(cmconfig?(m))
== & (let & ((null(cmconfig-list(m))))
== & (let & es-loc(es; e) = last(cmconfig-list(m))  Id;i.(cmconfig?(m))
== & (let & (index:{0..||cmconfig-list(m)||}
== & (let & (((0 < index)
== & (let & (& es-loc(es; e) = cmconfig-list(m)[index]  Id
== & (let & (& i = cmconfig-list(m)[(index - 1)]  Id));i,n.(cmseq?(m))
== & (let & i = cmseq-to(m)  Id
== & (let & es-loc(es; e) = cmseq-from(m)  Id
== & (let & n = cmseq-num(m)  )) 

latex

Definitions	(e < e'), P  Q, (e <loc e'), x:A. B(x), E(X), let x = a in b(x), f(a), chain_config_ind(x;head;tail;id.pred(id);id,num.succ(id;num)), X(e), i  j , hd(l), A, null(as), last(L), cmconfig?(x), x:A. B(x), {i..j}, ||as||, a < b, l[i], n - m, #$n, cmconfig-list(x), b, cmseq?(x), cmseq-to(x), P & Q, Id, loc(e), cmseq-from(x), s = t, , cmseq-num(x)
FDL editor aliases	config-antecedent